module Zeno.Checker ( falsifiable,
                      purifyConditions ) where

import Prelude ()
import StdImports

import Zeno.Core
import Zeno.Term
import Zeno.Clause
import Zeno.Evaluation
import Zeno.Function

import qualified Data.Set as Set

falsifiable :: ZClause -> ZenoReader Bool
falsifiable cls = do
  let Clause eq@(l_term `Equals` r_term) conds = 
        fst $ runWriter $ applyTermDefinitions [] cls
  let conds' = filter (not . equal) conds
  if null conds' && unequal eq
      then return True
    else if any unequal conds' || equal eq
      then return False
    else do
      let all_terms = l_term : r_term : map equalityLeft conds'
          all_crits = filter (\t -> usableCriticalTerm t || null (snd t)) 
                    $ mergeCriticalTerms
                    $ mapMaybe (runWriterT . deepCriticalTerm)
                    $ all_terms
      case all_crits of
        [] -> return False
        cterm@(term, _) : _ -> do
          let new_clause = Clause eq conds'
          let Just cons_s = instantiateConstructors cterm
          stateful cons_s $ \cons ->
            or <$> mapM (falsify new_clause term) cons
  where
    falsify :: ZClause -> ZTerm -> (ZTerm, a) -> ZenoReader Bool
    falsify clause old_term (new_term, _) =
      falsifiable 
        $ substituteTakingSources old_term new_term clause
    
    deepCriticalTerm :: ZTerm -> WriterT [Id] Maybe ZTerm
    deepCriticalTerm term@(Var var) = lift $
      if destructibleVar var
        then Just term
        else Nothing
    deepCriticalTerm term = 
      case applyFunction [] term of
        Just (CaseOf id strict_term _) -> do
          tell [id]
          deepCriticalTerm strict_term
        _ -> 
          lift Nothing    
          
purifyConditions :: ZClause -> ZenoReader ZClause
purifyConditions (Clause eq conds) = do
  conds' <- tryRemove [] conds
  return (Clause eq conds')
  where
    tryRemove :: [ZEquality] -> [ZEquality] -> ZenoReader [ZEquality]
    tryRemove needed_cs [] = return needed_cs
    tryRemove needed_cs (c:cs) = do
      needed <- falsifiable (Clause eq (needed_cs ++ cs))
      if needed
        then tryRemove (c : needed_cs) cs
        else tryRemove needed_cs cs
    
    
